Nuprl Definition : es-first-since
11,40
postcript
pdf
e2
= first
e
e1
.
P
(
e
) == es-le(
es
;
e1
;
e2
)
P
(
e2
)
e
[
e1
,
e2
).
P
(
e
)
latex
clarification:
es-first-since(
es
;
e
.
P
(
e
);
e1
;
e2
) == es-le(
es
;
e1
;
e2
)
P
(
e2
)
all
e
from
es
in [
e1
;
e2
).
P
(
e
)
latex
Definitions
e2
= first
e
e1
.
P
(
e
)
,
es-le(
es
;
e
;
e'
)
,
P
Q
,
e
[
e1
,
e2
).
P
(
e
)
,
A
FDL editor aliases
es-first-since
origin